k(v:B) sends on l [tg:T, f <state, v>]?[]
== ((x:Id. vartype(source(l);x) r ds(x)?Top)
== & (e:E. (loc(e) = source(l))  (kind(e) = k)  (valtype(e) r B))
== & (e:E. (kind(e) = rcv(l,tg))  (valtype(e) r T)))
== c (e:E.
== c (loc(e) = source(l))
== c  (kind(e) = k)
== c  (((can-apply(f;<(state when e), val(e)>))
== c  (( (e':E
== c  (( (((kind(e') = rcv(l,tg))
== c  (( (c (sender(e') = e
== c  (( (c & (e'':E. (kind(e'') = rcv(l,tg))  (sender(e'') = e)  (e'' = e'))
== c  (( (c & val(e') = do-apply(f;<(state when e), val(e)>)))))
== c  & (((can-apply(f;<(state when e), val(e)>)))
== c  & ( ((e':E. ((kind(e') = rcv(l,tg)) c (sender(e') = e))))))) 

latex

---

clarification:

conditional-send-p(es;ds;k;B;l;tg;T;f)
== ((x:Id. es-vartype(es; source(l); x) r fpf-cap(ds;IdDeq;x;Top))
== & (e:es-E(es).
== & ((es-loc(es; e) = source(l)  Id)  (es-kind(es; e) = k  Knd)  (es-valtype(es; e) r B))
== & (e:es-E(es). (es-kind(es; e) = rcv(l,tg)  Knd)  (es-valtype(es; e) r T)))
== c (e:es-E(es).
== c (es-loc(es; e) = source(l)  Id)
== c  (es-kind(es; e) = k  Knd)
== c  (((can-apply(f;<es-state-when(es;e), es-val(es; e)>))
== c  (( (e':es-E(es)
== c  (( (((es-kind(es; e') = rcv(l,tg)  Knd)
== c  (( (c (es-sender(es; e') = e  es-E(es)
== c  (( (c & (e'':es-E(es).
== c  (( (c & ((es-kind(es; e'') = rcv(l,tg)  Knd)
== c  (( (c & ( (es-sender(es; e'') = e  es-E(es))
== c  (( (c & ( (e'' = e'  es-E(es)))
== c  (( (c & es-val(es; e') = do-apply(f;<es-state-when(es;e), es-val(es; e)>)  T))))
== c  & (((can-apply(f;<es-state-when(es;e), es-val(es; e)>)))
== c  & ( ((e':es-E(es)
== c  & ( ((((es-kind(es; e') = rcv(l,tg)  Knd)
== c  & ( ((c (es-sender(es; e') = e  es-E(es)))))))) 

latex

Definitions	vartype(i;x), f(x)?z, IdDeq, Top, valtype(e), Id, loc(e), source(l), P & Q, x:A. B(x), do-apply(f;x), P  Q, b, can-apply(f;x), <a, b>, (state when e), val(e), A, x:A. B(x), A c B, Knd, kind(e), rcv(l,tg), s = t, E, sender(e)
FDL editor aliases	conditional-send-p